$\forall$$T$:Type\{i\}, $x$:$T$, $L$:($T$ List), $P$:($T$$\rightarrow$$T$$\rightarrow$prop\{i':l\}).
\\[0ex]pairwise($x$,$y$.$P$($x$,$y$); cons($x$; $L$)) $\Leftarrow\!\Rightarrow$ (pairwise($x$,$y$.$P$($x$,$y$); $L$) $\wedge$ l\_all($L$; $T$; $y$.$P$($x$,$y$)))